In the first-order logic theorem prover， clause preprocessing is an essential step， and the rule of clause elimination is an extremely important part of preprocessing. The traditional clause elimination method based on pure literal rules has some drawbacks which more than enough clauses should be deleted in theory， while less clauses were deleted during implementation. In order to make the clause elimination more accurate， the clauses were classified based on pure literal rules. The first category was called the invalid clause which was not able to form complementary pair to any clause in the clause set through equivalence substitution， and should be completely deleted. The second category was called the relatively invalid clause， which was not complementary to any clause in the current clause set， but could be replaced by other clause after equivalence substitution and should be deleted after certain deduction steps. The clause elimination should actually be a dynamic process where the current clause elimination would affect the invalidity of the determined clauses. Therefore， a clause elimination recursive traversal algorithm for determining clause invalidity was presented and implemented to the prover CSE1.5 （Contradiction Separation Extension 1.5）. The problems in first-order logic problem group of the CADE （Conference on Automated DEduction） Automated Theorem Proving （ATP） system competition from 2019 to 2022 were used as the test problems. The CSE1.5_IC with the invalid clause elimination algorithm proved 27 more problems than original CSE1.5 in 300 s. Among all the FNE （FOF theorems without Equality） test cases jointly proved by the two versions of the prover， CSE1.5_IC eliminated 28 more invalid clauses per problem on average than CSE1.5， and the average solution time was reduced by 7.07 s. The experimental results show that the proposed invalid clause elimination algorithm is an effective preprocessing method， which increases the reduction accuracy in the first-order logical clause set， and improves the proving ability and shortens the proof time of automatic theorem prover.

The fake speech produced by modern speech synthesis and timbre conversion systems poses a serious threat to the automatic speaker recognition system. Most of the existing fake speech detection systems perform well for the known attack types in the training process， but degrades significantly in detecting unknown attack types in practical applications. Therefore， combined with the recently proposed Dual?Path Res2Net （DP?Res2Net）， a semi?supervised end?to?end fake speech detection method based on time?domain waveforms was proposed. Firstly， semi?supervised learning was adopted for domain transfer to reduce the difference of data distribution between training set and test set. Then， for feature engineering， time-domain sampling points were input into DP?Res2Net directly， which increased the local multi?scale information and made full use of the dependence between audio segments. Finally， the embedded tensors were obtained to judge fake speech from natural speech after the input features going through the shallow convolution module， feature fusion module and global average pooling module. The performance of the proposed method was evaluated on the publicly available ASVspoof 2021 Speech Deep Fake evaluation set as well as the dataset VCC （Voice Conversion Challenge）. Experimental results show that the Equal Error Rate （EER） of the proposed method is 19.97%， which is 10.8% less than that of the official optimal baseline system， verifying that the semi?supervised end?to?end fake speech detection method based on time?domain waveforms is effective when recognizing unknown attacks and has higher generalization capability.

Current Internet of Things (IoT) networks have high detection rate of known types of attacks but the network node energy consumption is high. Aiming at this fact, an intrusion detection approach based on Practical Byzantine Fault Tolerance (PBFT) algorithm was proposed. Firstly, Support Vector Machine (SVM) was used for pre-training to obtain the intrusion detection decision rule, and the trained rule was applied to each node in IoT. Then, some nodes were voted to perform the active intrusion detection on other nodes in the network, while announce their detection results to other nodes. Finally, each node judged the state of other nodes according to PBFT algorithm, making the detection results reach consistency in the system. The simulation results on NSL-KDD dataset by TinyOS show that the proposed approach reduces the energy consumption by 12.2% and 7.6% averagely and respectively compared with Integrated Intrusion Detection System (ⅡDS) and Two-layer Dimension reduction and Two-tier Classification (TDTC) approach, effectively reducing the energy consumption of IoT.

Focusing on low accuracy and high costs of backtracking-based subgraph query algorithm applied to large-scale graphs, a Spark-based Subgraph Query Matching (SQM) algorithm was proposed to improve query accuracy and reduce query overhead for large graphs. The data graph was firstly filtered according to structure information, and the query graph was divided into basic query units. Then each basic query unit was matched and joined together. Finally, the algorithm's efficiency was improved and search space was reduced by parallelization. The experimental results show that compared with Stwig (Sub twig) algorithm and TurboISO algorithm, SQM algorithm can increase the speed by 50% while ensuring the same query results.

As a type of data structure representing entities, graphs are widely used in fields that have high requirements on data relevance, such as community data discovery, biochemical analysis and social security analysis. Focusing on the issue of real-time graph query operation under large-scale data, building a suitable index can effectively reduce query response time and improve query accuracy. The basic structure of index-based subgraph query algorithm was firstly introduced and then state-of-the-art algorithms were divided into two categories by construction method of index:enumeration construction and frequent pattern mining construction. Then these algorithms were introduced and analyzed from three aspects:index features, index structures and application datasets. Finally, main problems toward index-based subgraph query algorithm were summarized and analyzed, the latest query technology based on the distributed system was briefly described, and the future trend was forecasted.

To improve the performance of feature selection under the unsupervised scenario, the relationship between the distribution of the first K minimal eigenvalues for a normalized graph Laplacian matrix and the structure of the clusters was identified, and a new feature selection algorithm based on the spectral analysis was proposed. The feature selection algorithm might be time-consuming; hence the Nystrm method was applied to reduce the computational cost of the eigen-decomposition. The experiments on synthetic and real-world data sets show the efficiency of the proposed approach.